[<sup class="entry">TPIL</sup>](https://leanprover.github.io/theorem_proving_in_lean/{{page}})